;;;===========================================================================
;;;
;;; Algebraic Structures
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV: 
;;;
;;; Start date: 22/04/10 || End date: 24/04/10
;;;
;;;===========================================================================

(in-package "ACL2")

(include-book "data-structures/structures" :dir :system)

;;;***************************************************************************
;;;
;;; Magma
;;;
;;;***************************************************************************


#|

A magma is a set, together with a binary operation that satisfies:

Closure:
 For all a and b in the set, the result of the binary operation
 is also in the set.

|#


(defstructure magma inv binary-op)


(defun closure-binary-op (inv binary-op)
  (cons 'implies
	(cons (cons 'and 
		    (cons (cons inv (cons 'x 'nil))
			  (cons (cons inv (cons 'y 'nil)) 'nil)))
	      (cons (cons inv (cons (cons binary-op
					   (cons 'x (cons 'y 'nil)))
				     'nil)) 'nil))))

(defun magma-algebraic-structure (inv binary-op)
  (closure-binary-op inv binary-op))


(defmacro defmagma (inv binary-op name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-magma"))
		       'string)
	       name)
	      (cons (magma-algebraic-structure inv binary-op)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))

(defun check-magma-aux (magma name hints)
  `(list 'defmagma
	(magma-inv ,magma) 
	(magma-binary-op ,magma) 	
	,name
	:hints ,hints))


(defmacro check-magma-p (magma name &key hints)
  (cons 'make-event 
	(cons (check-magma-aux magma name hints) 'nil)))






#| 

Example:

(defun inv-unit (a)
  (equal a 0))

(defun binary-op-unit (a b)
  (declare (ignore a b))
  0)

(check-magma-p (make-magma :inv 'inv-unit :binary-op 'binary-op-unit) 'unit)

|#
	


;;;***************************************************************************
;;;
;;; Semigroup
;;;
;;;***************************************************************************


#|

A semigroup is an associative magma

|#


(defstructure semigroup inv binary-op)

(defun associativity-binary-op (inv binary-op)
  (cons 'implies
      (cons (cons 'and 
                  (cons (cons inv (cons 'x 'nil))
                        (cons (cons inv (cons 'y 'nil)) 
                              (cons (cons inv (cons 'z 'nil))
                                    'nil))))
            (cons (cons 'equal (cons (cons binary-op 
                                           (cons (cons binary-op
                                                       (cons 'x (cons 'y 'nil)))
                                                 (cons 'z 'nil))) 
                                     (cons (cons binary-op 
						 (cons 'x      
						       (cons (cons binary-op
								   (cons 'y (cons 'z 'nil)))
							     'nil
							     ))) 'nil)))
                  'nil))
      ))
  

(defun semigroup-algebraic-structure (inv binary-op)
  (cons 'and 
	(cons (magma-algebraic-structure inv binary-op)
	      (cons (associativity-binary-op inv binary-op) 'nil)
		    )))



(defmacro defsemigroup (inv binary-op name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-semigroup"))
		       'string)
	       name)
	      (cons (semigroup-algebraic-structure inv binary-op)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))



(defun check-semigroup-aux (semigroup name hints)
  `(list 'defsemigroup
	(semigroup-inv ,semigroup) 
	(semigroup-binary-op ,semigroup) 	
	,name
	:hints ,hints))


(defmacro check-semigroup-p (semigroup name &key hints)
  (cons 'make-event 
	(cons (check-semigroup-aux semigroup name hints) 'nil)))



#| 

Example:

(defun inv-unit (a)
  (equal a 0))

(defun binary-op-unit (a b)
  (declare (ignore a b))
  0)

(check-semigroup-p (make-semigroup :inv 'inv-unit :binary-op 'binary-op-unit) 'unit)

|#





;;;***************************************************************************
;;;
;;; Monoid
;;;
;;;***************************************************************************


#|

A monoid is a semigroup with an identity element

|#

(defstructure monoid inv binary-op id-elem)


(defun identity-element-binary-op-left (inv binary-op id-elem)
  (cons 'implies
      (cons (cons inv (cons 'x 'nil)) 
            (cons (cons 'equal (cons (cons binary-op
                                           (cons (cons id-elem 'nil) (cons 'x 'nil))) 
                                     (cons 'x 'nil)))
                  'nil))
      ))


(defun identity-element-binary-op-right (inv binary-op id-elem)
  (cons 'implies
      (cons (cons inv (cons 'x 'nil)) 
            (cons (cons 'equal (cons (cons binary-op
                                           (cons 'x (cons (cons id-elem 'nil) 'nil))) 
                                     (cons 'x 'nil)))
                  'nil))
      ))


(defun inv-identity-element (inv id-elem)
  (cons inv (cons (cons id-elem 'nil) 'nil)))
  

(defun monoid-algebraic-structure (inv binary-op id-elem)
  (cons 'and 
	(cons (semigroup-algebraic-structure inv binary-op)
	      (cons (identity-element-binary-op-left inv binary-op id-elem)
		    (cons (identity-element-binary-op-right inv binary-op id-elem)
			  (cons (inv-identity-element inv id-elem) 'nil))))))
			


(defmacro defmonoid (inv binary-op id-elem name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-monoid"))
		       'string)
	       name)
	      (cons (monoid-algebraic-structure inv binary-op id-elem)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))



(defun check-monoid-aux (monoid name hints)
  `(list 'defmonoid
	(monoid-inv ,monoid) 
	(monoid-binary-op ,monoid) 
	(monoid-id-elem ,monoid)
	,name
	:hints ,hints))


(defmacro check-monoid-p (monoid name &key hints)
  (cons 'make-event 
	(cons (check-monoid-aux monoid name hints) 'nil)))




#| 

Example:

(defun inv-unit (a)
  (equal a 0))

(defun binary-op-unit (a b)
  (declare (ignore a b))
  0)

(defun id-elem-unit ()
  0)


(check-monoid-p (make-monoid :inv 'inv-unit 
			     :binary-op 'binary-op-unit
			     :id-elem 'id-elem-unit) 'unit)



|#


;;;***************************************************************************
;;;
;;; Group
;;;
;;;***************************************************************************


#|

A group is a monoid with inverse

|#


(defstructure group inv binary-op id-elem inverse)

(defun inverse-binary-op-left (inv binary-op id-elem inverse)
  (cons 'implies
      (cons (cons inv (cons 'x 'nil)) 
            (cons (cons 'equal (cons (cons binary-op
                                           (cons (cons inverse (cons 'x 'nil))
						 (cons 'x 'nil))) 
                                     (cons (cons id-elem 'nil) 'nil)))
                  'nil))
      ))


(defun inverse-binary-op-right (inv binary-op id-elem inverse)
  (cons 'implies
      (cons (cons inv (cons 'x 'nil)) 
            (cons (cons 'equal (cons (cons binary-op
                                           (cons 'x (cons (cons inverse (cons 'x 'nil))'nil)))	
				     (cons (cons id-elem 'nil) 'nil))) 'nil))
      ))
      


(defun inv-inverse (inv inverse)
  (cons 'implies
      (cons (cons inv (cons 'x 'nil))
	    (cons (cons inv (cons (cons inverse (cons 'x 'nil)) 'nil)) 'nil))))
  

(defun group-algebraic-structure (inv binary-op id-elem inverse)
  (cons 'and 
	(cons (monoid-algebraic-structure inv binary-op id-elem)
	      (cons (inverse-binary-op-left inv binary-op id-elem inverse)
		    (cons (inverse-binary-op-right inv binary-op id-elem inverse)
			  (cons (inv-inverse inv inverse) 'nil))))))
			

(defmacro defgroup (inv binary-op id-elem inverse name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-group"))
		       'string)
	       name)
	      (cons (group-algebraic-structure inv binary-op id-elem inverse)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))



(defun check-group-aux (group name hints)
  `(list 'defgroup
	(group-inv ,group) 
	(group-binary-op ,group) 
	(group-id-elem ,group)
	(group-inverse ,group)
	,name
	:hints ,hints))


(defmacro check-group-p (group name &key hints)
  (cons 'make-event 
	(cons (check-group-aux group name hints) 'nil)))



#| 

Example:

(defun inv-unit (a)
  (equal a 0))

(defun binary-op-unit (a b)
  (declare (ignore a b))
  0)

(defun id-elem-unit ()
  0)


(defun inverse-unit (x)
  (declare (ignore x))
  0)


(check-group-p (make-group :inv 'inv-unit 
			   :binary-op 'binary-op-unit
			   :id-elem 'id-elem-unit
			   :inverse 'inverse-unit) 'unit)

|#


#|
(encapsulate
 (((inv *) => *)
  ((binary-op * *) => *)
  ((id-elem ) => *)
  ((inverse *) => *))

 (local (defun inv (a)
  (equal a 0)))

(local (defun binary-op (a b)
  (declare (ignore a b))
  0))

(local (defun id-elem ()
  0))


(local (defun inverse (x)
  (declare (ignore x))
  0))
 

(check-group-p (make-group :inv 'inv
			   :binary-op 'binary-op
			   :id-elem 'id-elem
			   :inverse 'inverse) 'group)

)



(defthm [a*[a^{-1}*b]]*b^{-1}=unit
  (implies (and (inv a)
		(inv b))
	   (equal (binary-op (binary-op a (binary-op (inverse a) b)) (inverse b))
		  (id-elem))))




(defun inv-binary (a) (or (equal a 0) (equal a 1)))
(defun mult-binary (a b) (if (equal (+ a b) 2) 0 (+ a b)))
(defun inverse-binary (a) a)
(defun unit-binary () 0)



(check-group-p (make-group :inv 'inv-binary 
			   :binary-op 'mult-binary
			   :id-elem 'unit-binary
			   :inverse 'inverse-binary) 'binary)

(defthm [a*[a^{-1}*b]]*b^{-1}=unit-binary
  (implies (and (inv-binary a)
		(inv-binary b))
	   (equal (mult-binary
		   (mult-binary a
				(mult-binary (inverse-binary a) b))
		   (inverse-binary b))
		  (unit-binary)))
  :hints (("Goal" :by (:functional-instance [a*[a^{-1}*b]]*b^{-1}=unit
					    (inv inv-binary)
					    (binary-op mult-binary)
					    (inverse inverse-binary)
					    (id-elem unit-binary)))))

|#


;;;***************************************************************************
;;;
;;; Abelian Group
;;;
;;;***************************************************************************


#|

An abelian group is a group with commutativity property

|#

(defstructure abgroup inv binary-op id-elem inverse)


(defun commutativity-binary-op (inv binary-op)
  (cons 'implies
	(cons (cons 'and 
                  (cons (cons inv (cons 'x 'nil))
                        (cons (cons inv (cons 'y 'nil)) 'nil)))
	      (cons (cons 'equal (cons (cons binary-op
						   (cons 'x (cons 'y 'nil)))
				 
				 (cons (cons binary-op
						   (cons 'y (cons 'x 'nil))) 'nil))) 'nil)
	      )))


  

(defun abelian-group-algebraic-structure (inv binary-op id-elem inverse)
  (cons 'and 
	(cons (group-algebraic-structure inv binary-op id-elem inverse)
	      (cons (commutativity-binary-op inv binary-op) 'nil))))
			

(defmacro defabgroup (inv binary-op id-elem inverse name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-an-abelian-group"))
		       'string)
	       name)
	      (cons (abelian-group-algebraic-structure inv binary-op id-elem inverse)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))



(defun check-abgroup-aux (group name hints)
  `(list 'defgroup
	(group-inv ,group) 
	(group-binary-op ,group) 
	(group-id-elem ,group)
	(group-inverse ,group)
	,name
	:hints ,hints))


(defmacro check-abgroup-p (group name &key hints)
  (cons 'make-event 
	(cons (check-abgroup-aux group name hints) 'nil)))

#| 

Example:

(defun inv-unit (a)
  (equal a 0))

(defun binary-op-unit (a b)
  (declare (ignore a b))
  0)

(defun id-elem-unit ()
  0)


(defun inverse-unit (x)
  (declare (ignore x))
  0)

(check-abgroup-p (make-abgroup :inv 'inv-unit 
			   :binary-op 'binary-op-unit
			   :id-elem 'id-elem-unit
			   :inverse 'inverse-unit) 'unit)





|#


;;;***************************************************************************
;;;
;;; Ring
;;;
;;;***************************************************************************


#|

A ring (R,+,·) is an abelian group under addition and a
monoid under product; moreover it must satisfy the distributy rules:

1. For all a, b and c in R, the equation a · (b + c) = (a · b) + (a · c) holds.
2. For all a, b and c in R, the equation (a + b) · c = (a · c) + (b · c) holds.

|#


(defstructure ring
   inv sum-binary-op id-elem inverse
   product-binary-op unit)


(defun distributivity-law-1 (inv sum-binary-op prod-binary-op)
  `(implies (and (,inv x) (,inv y) (,inv z))
	    (equal (,prod-binary-op x (,sum-binary-op y z))
		   (,sum-binary-op (,prod-binary-op x y) (,prod-binary-op x z)))))
  


(defun distributivity-law-1 (inv sum-binary-op prod-binary-op)
  (cons 'implies
	(cons (cons 'and 
                  (cons (cons inv (cons 'x 'nil))
                        (cons (cons inv (cons 'y 'nil))
			      (cons (cons inv (cons 'z 'nil)) 'nil))))
	      (cons (cons 'equal
			  (cons (cons prod-binary-op 
				      (cons 'x (cons (cons sum-binary-op (cons 'y (cons 'z 'nil))) 'nil)))
				(cons (cons sum-binary-op
					    (cons (cons prod-binary-op (cons 'x (cons 'y 'nil)))
						  (cons (cons prod-binary-op (cons 'x (cons 'z 'nil)) )'nil)))
				      'nil)
				)
			  ) 'nil))))


(defun distributivity-law-2 (inv sum-binary-op prod-binary-op)
  (cons 'implies
	(cons (cons 'and 
                  (cons (cons inv (cons 'x 'nil))
                        (cons (cons inv (cons 'y 'nil))
			      (cons (cons inv (cons 'z 'nil)) 'nil))))
	      (cons (cons 'equal
			  (cons (cons prod-binary-op 
				      (cons (cons sum-binary-op (cons 'x (cons 'y 'nil))) (cons 'z 'nil)))
				(cons (cons sum-binary-op
					    (cons (cons prod-binary-op (cons 'x (cons 'z 'nil)))
						  (cons (cons prod-binary-op (cons 'y (cons 'z 'nil)) )'nil)))
				      'nil)
				)
			  ) 'nil))))


  

(defun ring-algebraic-structure (inv sum-binary-op id-elem inverse prod-binary-op unit-elem)
  (cons 'and 
	(cons (group-algebraic-structure inv sum-binary-op id-elem inverse)
	      (cons (monoid-algebraic-structure inv prod-binary-op unit-elem) 
		    (cons (distributivity-law-1 inv sum-binary-op prod-binary-op)
			  (cons (distributivity-law-2 inv sum-binary-op prod-binary-op)
				'nil))))))
			

(defmacro defring (inv sum-binary-op id-elem inverse prod-binary-op unit-elem name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-ring"))
		       'string)
	       name)
	      (cons (ring-algebraic-structure inv sum-binary-op id-elem inverse prod-binary-op unit-elem)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))



(defun check-ring-aux (ring name hints)
  `(list 'defring
	(ring-inv ,ring) 
	(ring-sum-binary-op ,ring) 
	(ring-id-elem ,ring)
	(ring-inverse ,ring)
	(ring-product-binary-op ,ring) 
	(ring-unit ,ring)
	,name
	:hints ,hints))


(defmacro check-ring-p (ring name &key hints)
  (cons 'make-event 
	(cons (check-ring-aux ring name hints) 'nil)))





#| 

Example:

 (defun inv-ring (a)
	  (integerp a))
 
 ;; Addition operation Z 

(defun addition-ring (a b)
	  (+ a b))

 ;; Product operation ring
 (defun product-ring (a b)
	  (* a b))

 ;; Inverse addition
  (defun inverse (a)
	  (- a))

 ;; Zero element ring
 (defun zero-element nil
	  0)

 ;; Unit element ring
  (defun unit nil
	  1)

(check-ring-p (make-ring :inv 'inv-ring
			   :sum-binary-op 'addition-ring
			   :id-elem 'zero-element
			   :inverse 'inverse
			   :product-binary-op 'product-ring
			   :unit 'unit) 'Z)


|#



